X:Type, eq:EqDecider(X), f, g:x:X fp Type, x:X, z:g(x)?Void.
f || g  (f(x)?Void r g(x)?Void) 

latex

Definitions	t  T, x:A. B(x), b, A, b, , s = t, , Type, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), x  dom(f), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, f(x)?z, f || g, EqDecider(T), Void, f(x), <a, b>, False, {T}, SQType(T), s ~ t, P  Q
Lemmas	bool cases, bool sq, fpf-ap wf, fpf-compatible wf, fpf-cap wf, fpf wf, deq wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf